Application: Automated Programming

The goal of automated programming is to accelerate software development by (semi-)automating the process of writing code and tests.

In property-based testing, a property such as "sorting a list does not change the length of a list" are stated that should be correct for a sorting function, and then the function is tested with randomly generated lists to see whether a counter example can be found that invalidates the property to make the test fail, otherwise the test is passed.

In a project, we could investigate and implement some procedure for automated generation of data following some techniques from a paper. For the seminar, a few recent papers on this topic would be the following -- depending on your interest we might find older or more recent other papers as well:

• A completely unique account of enumeration
• Logarithm and program testing
• Parsing Randomness

The goal of program synthesis is to turn a high-level specification of a problem into a program, ideally an efficient one. This usually involves searching through the (very large) space of possible programs to find the ones that satisfy our requirements. One approach is to turn the search problem into a set of logical formulas. These are then passed to an off-the-shelf SMT (Satisfiability-Modulo-Theories) solver, which (hopefully) produces a solution that satisfies the formulas. Searching through the space of programs can also be done through rewriting, where we replace part of a program with an equivalent expression. A data structure called E-Graph allows storing many similar terms in a compact fashion, making the search, also called equality saturation, more tractable.

Recently, efficient frameworks for equality saturation have been developed in Rust and Julia. These frameworks also support program analysis, where properties of the programs are inferred to aid with rewriting. Equality saturation has shown promise in making floating point computations more numerically stable and in optimizing linear algebra programs.

• Growing solver-aided languages with Rosette
• Better Together: Unifying Datalog and Equality Saturation
• babble: Learning Better Abstractions with E-Graphs and Anti-Unification
• Metatheory. jl: Fast and elegant algebraic computation in Julia with extensible equality saturation
• Optimizing Recursive Queries with Program Synthesis
• Languages with Decidable Learning: A Meta-theorem